Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    dbl(0)  → 0
2:    dbl(s(X))  → s(n__s(n__dbl(activate(X))))
3:    dbls(nil)  → nil
4:    dbls(cons(X,Y))  → cons(n__dbl(activate(X)),n__dbls(activate(Y)))
5:    sel(0,cons(X,Y))  → activate(X)
6:    sel(s(X),cons(Y,Z))  → sel(activate(X),activate(Z))
7:    indx(nil,X)  → nil
8:    indx(cons(X,Y),Z)  → cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))
9:    from(X)  → cons(activate(X),n__from(n__s(activate(X))))
10:    s(X)  → n__s(X)
11:    dbl(X)  → n__dbl(X)
12:    dbls(X)  → n__dbls(X)
13:    sel(X1,X2)  → n__sel(X1,X2)
14:    indx(X1,X2)  → n__indx(X1,X2)
15:    from(X)  → n__from(X)
16:    activate(n__s(X))  → s(X)
17:    activate(n__dbl(X))  → dbl(X)
18:    activate(n__dbls(X))  → dbls(X)
19:    activate(n__sel(X1,X2))  → sel(X1,X2)
20:    activate(n__indx(X1,X2))  → indx(X1,X2)
21:    activate(n__from(X))  → from(X)
22:    activate(X)  → X
There are 18 dependency pairs:
23:    DBL(s(X))  → S(n__s(n__dbl(activate(X))))
24:    DBL(s(X))  → ACTIVATE(X)
25:    DBLS(cons(X,Y))  → ACTIVATE(X)
26:    DBLS(cons(X,Y))  → ACTIVATE(Y)
27:    SEL(0,cons(X,Y))  → ACTIVATE(X)
28:    SEL(s(X),cons(Y,Z))  → SEL(activate(X),activate(Z))
29:    SEL(s(X),cons(Y,Z))  → ACTIVATE(X)
30:    SEL(s(X),cons(Y,Z))  → ACTIVATE(Z)
31:    INDX(cons(X,Y),Z)  → ACTIVATE(X)
32:    INDX(cons(X,Y),Z)  → ACTIVATE(Y)
33:    INDX(cons(X,Y),Z)  → ACTIVATE(Z)
34:    FROM(X)  → ACTIVATE(X)
35:    ACTIVATE(n__s(X))  → S(X)
36:    ACTIVATE(n__dbl(X))  → DBL(X)
37:    ACTIVATE(n__dbls(X))  → DBLS(X)
38:    ACTIVATE(n__sel(X1,X2))  → SEL(X1,X2)
39:    ACTIVATE(n__indx(X1,X2))  → INDX(X1,X2)
40:    ACTIVATE(n__from(X))  → FROM(X)
The approximated dependency graph contains one SCC: {24-34,36-40}.
Tyrolean Termination Tool  (6.48 seconds)   ---  May 3, 2006